FDL - Step of Proof: p-fun-exp-compose

Step of Proof: p-fun-exp-compose

11,40

Inference at *
Iof proof for Lemma p-fun-exp-compose:

T:Type, n:

, h, f:(T

(T + Top)). f^n o h = primrec(n;h;

i,g. f o g )

by (InductionOnNat)

CollapseTHEN (RepUR ``p-fun-exp`` ( 0)

)

C1:

C1: 1. T : Type

C1:

h, f:(T

(T + Top)). p-id() o h = h

C2:

C2: 1. T : Type

C2: 2. n :

C2: 3. 0 < n

C2: 4.

h, f:(T

(T + Top)). f^n - 1 o h = primrec(n - 1;h;

i,g. f o g )

C2:

h, f:(T

(T + Top)). primrec(n;p-id();

i,g. f o g ) o h = primrec(n;h;

i,g. f o g )

Definitions Void, a < b, n - m, n+m, -n, #$n, A B, A, False, i j , P Q, {x:A| B(x)} , Type, x:A. B(x), s = t, left + right, Top, x:AB(x), t T, , f^n

Lemmas ge wf, nat properties, nat wf

Definitions	Void, a < b, n - m, n+m, -n, #$n, A B, A, False, i j , P Q, {x:A\| B(x)} , Type, x:A. B(x), s = t, left + right, Top, x:AB(x), t T, , f^n
Lemmas	ge wf, nat properties, nat wf